Nuprl Definition : ecl-trans-state-from
0,22
postcript
pdf
ecl-trans-state-from(
v
;
z
;
L
)
== let
T
,
ks
,
i
,
g
,
h
,
a
,
e
=
v
in
==
list_accum(
x
,
a
.
a
/
k
,
zz
.
zz
/
s
,
v
. if deq-member(KindDeq;
k
;
ks
)
g
(
k
,
s
,
v
,
x
) else
x
fi;
z
;
L
)
latex
Definitions
let
a
,
b
,
c
,
d
,
e
,
f
,
g
=
u
in
v
(
a
;
b
;
c
;
d
;
e
;
f
;
g
)
,
list_accum(
x
,
a
.
f
(
x
;
a
);
y
;
l
)
,
if
b
t
else
f
fi
,
deq-member(
eq
;
x
;
L
)
,
KindDeq
FDL editor aliases
ecl-trans-state-from
origin
g(k,s,v,x) else x fi;z;L) g(k,s,v,x) else x fi;z;L) t else f fi